($\lambda$$A$,$B$,$C$,$f$,$g$,$z$. $f$ o $g$) $\in$ $A$,$B$,$C$:Type$\rightarrow$($B$$\rightarrow$$C$)$\rightarrow$($A$$\rightarrow$$B$)$\rightarrow$($\downarrow$True)$\rightarrow$$A$$\rightarrow$$C$